(set-option :produce-unsat-model-interpolants true)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 15))
(let ((e3 (+ v1 v1)))
(let ((e4 (+ v1 e3)))
(let ((e5 (/ e2 (- e2))))
(let ((e6 (/ e2 e2)))
(let ((e7 (/ e2 e2)))
(let ((e8 (+ e6 v1)))
(let ((e9 (- e6)))
(let ((e10 (* e2 e6)))
(let ((e11 (- e9)))
(let ((e12 (+ e3 e5)))
(let ((e13 (* e5 v1)))
(let ((e14 (/ e2 e2)))
(let ((e15 (- e11)))
(let ((e16 (+ v0 e10)))
(let ((e17 (= e12 e15)))
(let ((e18 (distinct e15 e8)))
(let ((e19 (>= e8 e10)))
(let ((e20 (= v1 v1)))
(let ((e21 (distinct e13 e12)))
(let ((e22 (> e9 e3)))
(let ((e23 (>= e14 e3)))
(let ((e24 (> v0 e10)))
(let ((e25 (>= e10 e8)))
(let ((e26 (< e13 e10)))
(let ((e27 (< e10 e15)))
(let ((e28 (> e10 e5)))
(let ((e29 (>= e13 e3)))
(let ((e30 (distinct e5 e16)))
(let ((e31 (= v0 v1)))
(let ((e32 (distinct e6 e13)))
(let ((e33 (< e11 e12)))
(let ((e34 (<= e5 e3)))
(let ((e35 (> e4 e15)))
(let ((e36 (<= e15 e9)))
(let ((e37 (>= e6 e9)))
(let ((e38 (= e9 e3)))
(let ((e39 (distinct v0 e10)))
(let ((e40 (> e14 e15)))
(let ((e41 (> e12 e9)))
(let ((e42 (> e4 e6)))
(let ((e43 (> e15 e14)))
(let ((e44 (< e8 e13)))
(let ((e45 (< e10 e3)))
(let ((e46 (distinct e5 e12)))
(let ((e47 (<= e14 e16)))
(let ((e48 (>= e7 e11)))
(let ((e49 (ite e23 v0 e6)))
(let ((e50 (ite e26 e13 e13)))
(let ((e51 (ite e30 e15 e50)))
(let ((e52 (ite e43 e12 e9)))
(let ((e53 (ite e36 e8 v0)))
(let ((e54 (ite e32 e16 e10)))
(let ((e55 (ite e31 e7 e6)))
(let ((e56 (ite e35 v1 e3)))
(let ((e57 (ite e39 e4 e8)))
(let ((e58 (ite e47 e14 e4)))
(let ((e59 (ite e20 e5 e58)))
(let ((e60 (ite e48 e54 e5)))
(let ((e61 (ite e19 e11 e4)))
(let ((e62 (ite e29 e9 e60)))
(let ((e63 (ite e30 e10 e9)))
(let ((e64 (ite e24 e14 e52)))
(let ((e65 (ite e40 e49 e59)))
(let ((e66 (ite e34 e3 v1)))
(let ((e67 (ite e30 e65 e50)))
(let ((e68 (ite e28 e3 e52)))
(let ((e69 (ite e41 e58 v1)))
(let ((e70 (ite e45 e4 e12)))
(let ((e71 (ite e23 e54 e64)))
(let ((e72 (ite e39 e11 e16)))
(let ((e73 (ite e18 e65 e11)))
(let ((e74 (ite e27 e7 e51)))
(let ((e75 (ite e19 e59 e71)))
(let ((e76 (ite e25 e55 e54)))
(let ((e77 (ite e30 e67 e11)))
(let ((e78 (ite e21 e72 e13)))
(let ((e79 (ite e44 e3 e58)))
(let ((e80 (ite e33 e74 e5)))
(let ((e81 (ite e38 e13 e72)))
(let ((e82 (ite e32 e79 e6)))
(let ((e83 (ite e27 e15 e54)))
(let ((e84 (ite e42 e75 e62)))
(let ((e85 (ite e22 e84 e81)))
(let ((e86 (ite e45 e59 e52)))
(let ((e87 (ite e48 e82 e66)))
(let ((e88 (ite e46 e87 e68)))
(let ((e89 (ite e43 e58 e86)))
(let ((e90 (ite e27 e78 e3)))
(let ((e91 (ite e34 e52 e9)))
(let ((e92 (ite e37 e89 e16)))
(let ((e93 (ite e17 e6 e71)))
(let ((e94 (> e64 e66)))
(let ((e95 (distinct e56 e5)))
(let ((e96 (distinct e64 e71)))
(let ((e97 (distinct v0 e12)))
(let ((e98 (>= e70 e49)))
(let ((e99 (<= e60 e57)))
(let ((e100 (= e7 e50)))
(let ((e101 (>= e72 e84)))
(let ((e102 (distinct e53 e72)))
(let ((e103 (> e50 e74)))
(let ((e104 (>= e8 e74)))
(let ((e105 (= e83 e92)))
(let ((e106 (distinct e8 e93)))
(let ((e107 (> e50 e66)))
(let ((e108 (> e80 e90)))
(let ((e109 (distinct e14 e76)))
(let ((e110 (< e5 e76)))
(let ((e111 (>= e82 e83)))
(let ((e112 (distinct e88 e11)))
(let ((e113 (distinct e57 e49)))
(let ((e114 (>= e84 e66)))
(let ((e115 (< e3 e61)))
(let ((e116 (>= e89 e11)))
(let ((e117 (distinct e69 e86)))
(let ((e118 (>= e82 e75)))
(let ((e119 (> e78 e88)))
(let ((e120 (= e93 e81)))
(let ((e121 (< e11 e89)))
(let ((e122 (>= e81 e16)))
(let ((e123 (distinct e65 e58)))
(let ((e124 (distinct e86 e58)))
(let ((e125 (< e74 e90)))
(let ((e126 (<= e89 e81)))
(let ((e127 (< e92 e58)))
(let ((e128 (= e71 e93)))
(let ((e129 (>= e58 e88)))
(let ((e130 (<= e4 e55)))
(let ((e131 (< e86 e67)))
(let ((e132 (= e69 e90)))
(let ((e133 (<= e85 e70)))
(let ((e134 (= e5 e8)))
(let ((e135 (> e16 e4)))
(let ((e136 (< e52 e73)))
(let ((e137 (<= e61 e72)))
(let ((e138 (= e52 e63)))
(let ((e139 (= e82 e76)))
(let ((e140 (= e82 e84)))
(let ((e141 (< v1 e93)))
(let ((e142 (<= e55 e53)))
(let ((e143 (= e14 e6)))
(let ((e144 (> e58 e57)))
(let ((e145 (>= e75 e79)))
(let ((e146 (distinct e16 e93)))
(let ((e147 (<= e11 e84)))
(let ((e148 (= v0 e57)))
(let ((e149 (<= e4 e55)))
(let ((e150 (>= e88 e73)))
(let ((e151 (> e67 e8)))
(let ((e152 (<= e6 e3)))
(let ((e153 (> e79 e68)))
(let ((e154 (> e53 e16)))
(let ((e155 (>= e70 e3)))
(let ((e156 (< e12 e63)))
(let ((e157 (> e76 e49)))
(let ((e158 (distinct e80 e86)))
(let ((e159 (distinct e87 e56)))
(let ((e160 (>= e16 e88)))
(let ((e161 (<= e73 e58)))
(let ((e162 (distinct e70 e87)))
(let ((e163 (= e78 e54)))
(let ((e164 (> e77 e55)))
(let ((e165 (= e65 e56)))
(let ((e166 (> e85 e5)))
(let ((e167 (= e67 e8)))
(let ((e168 (distinct e4 e60)))
(let ((e169 (= e81 e51)))
(let ((e170 (<= e89 e14)))
(let ((e171 (< e13 e66)))
(let ((e172 (= e54 e8)))
(let ((e173 (distinct e62 e75)))
(let ((e174 (<= v0 e65)))
(let ((e175 (>= v1 e89)))
(let ((e176 (> e60 e75)))
(let ((e177 (= e5 e57)))
(let ((e178 (> e74 v0)))
(let ((e179 (= e8 e76)))
(let ((e180 (< e11 e10)))
(let ((e181 (<= e9 e10)))
(let ((e182 (< e6 e77)))
(let ((e183 (distinct e8 e80)))
(let ((e184 (distinct e52 e4)))
(let ((e185 (>= e89 e53)))
(let ((e186 (distinct e73 e63)))
(let ((e187 (< e13 e65)))
(let ((e188 (= e90 e54)))
(let ((e189 (> e70 e62)))
(let ((e190 (= e11 e85)))
(let ((e191 (<= e15 e8)))
(let ((e192 (distinct e84 e69)))
(let ((e193 (< e57 e82)))
(let ((e194 (> e70 v0)))
(let ((e195 (= e53 e77)))
(let ((e196 (> e57 e80)))
(let ((e197 (>= e54 e78)))
(let ((e198 (> e61 e65)))
(let ((e199 (distinct e5 e84)))
(let ((e200 (> e72 e54)))
(let ((e201 (distinct e8 e59)))
(let ((e202 (> e82 e9)))
(let ((e203 (>= e55 e5)))
(let ((e204 (<= e92 e52)))
(let ((e205 (< e89 e10)))
(let ((e206 (< e57 e12)))
(let ((e207 (= e58 e63)))
(let ((e208 (= e84 e69)))
(let ((e209 (<= e62 e15)))
(let ((e210 (distinct e60 e58)))
(let ((e211 (> e88 e68)))
(let ((e212 (>= e86 e73)))
(let ((e213 (< e74 e85)))
(let ((e214 (distinct v1 e53)))
(let ((e215 (distinct e50 e74)))
(let ((e216 (>= e76 e9)))
(let ((e217 (> e3 e65)))
(let ((e218 (= e4 e6)))
(let ((e219 (< e89 e62)))
(let ((e220 (distinct e71 e74)))
(let ((e221 (distinct e3 e64)))
(let ((e222 (<= e8 e71)))
(let ((e223 (< e65 e58)))
(let ((e224 (= e58 e6)))
(let ((e225 (> e60 e52)))
(let ((e226 (> e82 e49)))
(let ((e227 (< e56 e76)))
(let ((e228 (> e72 e90)))
(let ((e229 (< e75 e57)))
(let ((e230 (distinct e51 e3)))
(let ((e231 (<= e78 e51)))
(let ((e232 (>= e77 e66)))
(let ((e233 (distinct e84 e13)))
(let ((e234 (<= e71 e4)))
(let ((e235 (>= e92 e75)))
(let ((e236 (= e10 e89)))
(let ((e237 (< e63 e72)))
(let ((e238 (< e16 e90)))
(let ((e239 (= e11 e13)))
(let ((e240 (= e90 e64)))
(let ((e241 (< e78 e68)))
(let ((e242 (distinct e53 e90)))
(let ((e243 (distinct e74 e6)))
(let ((e244 (distinct e70 e93)))
(let ((e245 (> e77 e10)))
(let ((e246 (= e93 e5)))
(let ((e247 (<= e76 e68)))
(let ((e248 (> e92 e10)))
(let ((e249 (distinct e80 e12)))
(let ((e250 (< e58 e63)))
(let ((e251 (distinct e88 e61)))
(let ((e252 (<= e11 e68)))
(let ((e253 (> e8 e9)))
(let ((e254 (= e49 e16)))
(let ((e255 (distinct e64 e84)))
(let ((e256 (>= e66 e67)))
(let ((e257 (< e91 e90)))
(let ((e258 (xor e24 e220)))
(let ((e259 (not e107)))
(let ((e260 (xor e145 e203)))
(let ((e261 (=> e191 e251)))
(let ((e262 (not e237)))
(let ((e263 (not e106)))
(let ((e264 (xor e163 e105)))
(let ((e265 (not e226)))
(let ((e266 (ite e36 e236 e102)))
(let ((e267 (not e165)))
(let ((e268 (= e98 e94)))
(let ((e269 (or e213 e264)))
(let ((e270 (= e32 e189)))
(let ((e271 (ite e140 e248 e146)))
(let ((e272 (not e130)))
(let ((e273 (= e172 e214)))
(let ((e274 (xor e22 e168)))
(let ((e275 (ite e272 e101 e268)))
(let ((e276 (not e142)))
(let ((e277 (or e110 e229)))
(let ((e278 (and e43 e174)))
(let ((e279 (xor e221 e133)))
(let ((e280 (xor e176 e114)))
(let ((e281 (xor e117 e177)))
(let ((e282 (or e37 e183)))
(let ((e283 (=> e279 e257)))
(let ((e284 (or e17 e187)))
(let ((e285 (and e259 e282)))
(let ((e286 (ite e223 e269 e240)))
(let ((e287 (xor e256 e184)))
(let ((e288 (or e175 e224)))
(let ((e289 (not e252)))
(let ((e290 (and e246 e138)))
(let ((e291 (xor e38 e159)))
(let ((e292 (not e155)))
(let ((e293 (xor e188 e123)))
(let ((e294 (= e28 e136)))
(let ((e295 (and e209 e134)))
(let ((e296 (not e39)))
(let ((e297 (ite e109 e162 e33)))
(let ((e298 (not e233)))
(let ((e299 (= e19 e181)))
(let ((e300 (ite e273 e190 e263)))
(let ((e301 (=> e120 e160)))
(let ((e302 (ite e149 e247 e258)))
(let ((e303 (= e161 e129)))
(let ((e304 (=> e245 e215)))
(let ((e305 (and e201 e151)))
(let ((e306 (or e182 e42)))
(let ((e307 (=> e126 e241)))
(let ((e308 (=> e231 e234)))
(let ((e309 (not e289)))
(let ((e310 (= e23 e111)))
(let ((e311 (not e157)))
(let ((e312 (= e298 e99)))
(let ((e313 (not e281)))
(let ((e314 (xor e198 e197)))
(let ((e315 (xor e290 e274)))
(let ((e316 (and e285 e135)))
(let ((e317 (=> e46 e275)))
(let ((e318 (= e218 e260)))
(let ((e319 (ite e108 e242 e148)))
(let ((e320 (= e305 e141)))
(let ((e321 (and e185 e180)))
(let ((e322 (= e164 e250)))
(let ((e323 (=> e208 e317)))
(let ((e324 (xor e318 e113)))
(let ((e325 (xor e112 e158)))
(let ((e326 (or e179 e227)))
(let ((e327 (=> e303 e171)))
(let ((e328 (ite e127 e35 e262)))
(let ((e329 (and e276 e132)))
(let ((e330 (xor e277 e97)))
(let ((e331 (= e40 e232)))
(let ((e332 (or e124 e283)))
(let ((e333 (= e125 e255)))
(let ((e334 (xor e332 e173)))
(let ((e335 (and e150 e170)))
(let ((e336 (=> e333 e238)))
(let ((e337 (and e310 e280)))
(let ((e338 (xor e336 e309)))
(let ((e339 (ite e338 e314 e302)))
(let ((e340 (=> e286 e299)))
(let ((e341 (and e239 e337)))
(let ((e342 (or e178 e152)))
(let ((e343 (or e48 e244)))
(let ((e344 (= e316 e288)))
(let ((e345 (xor e312 e270)))
(let ((e346 (ite e243 e29 e21)))
(let ((e347 (and e200 e95)))
(let ((e348 (and e235 e119)))
(let ((e349 (or e156 e202)))
(let ((e350 (xor e291 e315)))
(let ((e351 (=> e18 e297)))
(let ((e352 (ite e330 e294 e326)))
(let ((e353 (xor e296 e195)))
(let ((e354 (= e204 e284)))
(let ((e355 (= e335 e339)))
(let ((e356 (xor e154 e266)))
(let ((e357 (= e206 e350)))
(let ((e358 (not e219)))
(let ((e359 (= e323 e352)))
(let ((e360 (= e30 e304)))
(let ((e361 (or e186 e103)))
(let ((e362 (= e104 e287)))
(let ((e363 (and e306 e265)))
(let ((e364 (=> e194 e334)))
(let ((e365 (ite e358 e353 e96)))
(let ((e366 (or e293 e311)))
(let ((e367 (and e216 e321)))
(let ((e368 (and e328 e41)))
(let ((e369 (=> e20 e300)))
(let ((e370 (ite e331 e363 e342)))
(let ((e371 (=> e271 e365)))
(let ((e372 (ite e147 e26 e354)))
(let ((e373 (=> e371 e343)))
(let ((e374 (= e345 e359)))
(let ((e375 (and e360 e340)))
(let ((e376 (xor e207 e355)))
(let ((e377 (xor e169 e295)))
(let ((e378 (=> e308 e122)))
(let ((e379 (and e45 e376)))
(let ((e380 (=> e324 e249)))
(let ((e381 (and e320 e366)))
(let ((e382 (and e301 e356)))
(let ((e383 (and e346 e307)))
(let ((e384 (xor e292 e372)))
(let ((e385 (= e370 e137)))
(let ((e386 (xor e377 e357)))
(let ((e387 (xor e369 e386)))
(let ((e388 (ite e382 e322 e364)))
(let ((e389 (or e47 e362)))
(let ((e390 (=> e378 e211)))
(let ((e391 (xor e327 e100)))
(let ((e392 (and e143 e196)))
(let ((e393 (=> e225 e391)))
(let ((e394 (= e349 e348)))
(let ((e395 (and e375 e383)))
(let ((e396 (=> e278 e199)))
(let ((e397 (xor e393 e166)))
(let ((e398 (ite e217 e396 e313)))
(let ((e399 (=> e25 e27)))
(let ((e400 (=> e192 e374)))
(let ((e401 (or e267 e344)))
(let ((e402 (=> e379 e230)))
(let ((e403 (not e329)))
(let ((e404 (= e210 e398)))
(let ((e405 (=> e395 e392)))
(let ((e406 (not e401)))
(let ((e407 (or e385 e367)))
(let ((e408 (not e381)))
(let ((e409 (=> e228 e347)))
(let ((e410 (xor e325 e368)))
(let ((e411 (not e212)))
(let ((e412 (or e400 e397)))
(let ((e413 (=> e388 e403)))
(let ((e414 (xor e405 e341)))
(let ((e415 (=> e34 e319)))
(let ((e416 (ite e404 e351 e402)))
(let ((e417 (xor e411 e222)))
(let ((e418 (ite e416 e415 e412)))
(let ((e419 (xor e417 e193)))
(let ((e420 (=> e253 e406)))
(let ((e421 (or e387 e115)))
(let ((e422 (or e409 e421)))
(let ((e423 (or e384 e139)))
(let ((e424 (ite e205 e205 e408)))
(let ((e425 (ite e153 e390 e44)))
(let ((e426 (not e118)))
(let ((e427 (ite e144 e361 e121)))
(let ((e428 (=> e261 e394)))
(let ((e429 (= e380 e414)))
(let ((e430 (= e419 e426)))
(let ((e431 (or e429 e428)))
(let ((e432 (not e424)))
(let ((e433 (xor e131 e432)))
(let ((e434 (=> e433 e413)))
(let ((e435 (= e128 e116)))
(let ((e436 (not e430)))
(let ((e437 (= e389 e373)))
(let ((e438 (=> e425 e167)))
(let ((e439 (ite e420 e31 e434)))
(let ((e440 (and e427 e399)))
(let ((e441 (= e438 e438)))
(let ((e442 (ite e440 e254 e440)))
(let ((e443 (= e439 e442)))
(let ((e444 (xor e437 e422)))
(let ((e445 (xor e443 e436)))
(let ((e446 (xor e423 e445)))
(let ((e447 (and e418 e410)))
(let ((e448 (not e435)))
(let ((e449 (or e431 e444)))
(let ((e450 (ite e447 e441 e407)))
(let ((e451 (and e449 e446)))
(let ((e452 (xor e451 e451)))
(let ((e453 (= e452 e450)))
(let ((e454 (not e453)))
(let ((e455 (= e454 e454)))
(let ((e456 (xor e455 e448)))
e456
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat-assuming-model (v0 v1) ((/ 33 65) (/ (- 76) (- 24))))
(get-unsat-model-interpolant)
